/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

//! ! ! ! ! ! ! ! //
//rseater writes:
// NEVER USED
// the only implementation of BLBackend is BLSATLab; this one might not even be up to spec anymore
// for why this is the case, see comment in BLBackend next to the USE_PSOLVER field
//! ! ! ! ! ! ! ! //

package alloy.bool;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.LineNumberReader;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.net.Socket;
import java.net.UnknownHostException;

import alloy.util.Dbg;
import alloy.util.EnvFailureException;
import alloy.util.TmpFiles;

/**
 * BLPSolver: Java interface to the PSolver satisfiability solver.
 * This is the new backend which will be used by alloy.
 * this extends the BLBackend class.
 * Given a {@link BooleanFormula}, can return a satisfying
 * assignment or report that the formula is not satisfiable.
 * Can enumerate and count satisfying assignments for satisfiable formulas.
 * <p>
 * Actual work is done by a native program called PSolver;
 * below, we refer to it as "the solver".  PSolver is a distributed SAT solver
 * which for now we will run in "degenerate" single-process mode
 * <p>
 * Note (May 2002): BLPSolver is currently not used -- it has been patched
 * to allow the system to compile, but needs to be reviewed before actually
 * putting it into use.  Only the {@link BLSATLab} implementation of
 * {@link BLBackend} is currently used.
 */
public class BLPSolver extends BLBackend {
    private Process _solverProcess;
    private Thread _solverWatchThread;
    private Thread _solverOutputReaderThread;

    // the Socket used for communicating with the solver
    private Socket _solverSocket;

        /** Solver's input stream, to which we write commands. */
    private PrintWriter _solverStdIn;
    /** Solver's output stream, from which we read solver status
    messages and results.  */
    private LineNumberReader _solverStdOut;

    // the process output streams
    private LineNumberReader _processOut;

    /** Whether {@link #solve} or {@link #next} is in progress.
    Currently the code is non-reentrant: once we start
    solving one formula, we cannot start solving another
    until this one either finishes or is cancelled. */
    private boolean _solveInProgress = false;

    /** Whether "cancel solving" command is in progress,
    i.e. {@link #interruptSolver} has been called but
    the currently running {@link #solve} or {@link #next}
    has not yet returned. */
    private boolean _cancelInProgress = false;

    private int _lastNumVars;

    private File _myTmpDir;

    private int _clientId;

    private static final String _solverMessageStart = "<<<";
    private static final String _solverMessageEnd = ">>>";

    private static final int TIMEOUT_INTERVAL = 10000;
    private static final int PROGRESS_INTERVAL = 5;

    private static final boolean RUN_SATSERVER = false;// temp - false to assume satserver already running
    private static final int PORTNUM = 5000; // port to run satserver on



    /** constructor - we now run the solver process every time */
    BLPSolver() { }

    /** send a one-line command to the solver */
    private synchronized void _sendSolverCmd(String cmd) {
    //System.out.println ("Solver check");
    _checkSolver();
    //System.out.println ("Sending solver command: " + cmd);
    _solverStdIn.println(cmd);
    //System.out.println ("Flush");
    _solverStdIn.flush();
    }

    protected BoolStencil _computeUnsatCore() { Dbg.fatal("unsupported operation"); return null; }

    /** read a result from the solver */
    private BLPSolverMessage _getSolverResult() {
    // scan for special string: [[[..]]]
    String s = null;
    do {
        try  { s = _solverStdOut.readLine();  }
        catch (Exception e) {
            Dbg.fail("Read error in BLSATLab.getSolverResult: " + e);
        }

        Dbg.info("SOLV: " + s);
        //alloy.report.Report.result(s);
        _checkSolver();
        if (s == null)
        return new BLPSolverMessage ();
        //System.out.println(s);
        Thread.yield();

    } while (s.indexOf(_solverMessageStart) == -1);
    return new BLPSolverMessage (s.substring(s.indexOf(_solverMessageStart)+_solverMessageStart.length(), s.indexOf(_solverMessageEnd)));
    }


    /** Start a new copy of the solver. */
    private void _startSolver(String configFileName_, String solverName_) {
    if (RUN_SATSERVER) {
      String executableExtension =
        (System.getProperty("os.name").toUpperCase().startsWith("WIN") ? ".exe" : "");
      try {
          String execLine = "." + File.separator + "satserver" +  executableExtension + " " + PORTNUM + " " + configFileName_ + " -singleclient " + solverName_.toLowerCase ();
        Dbg.info ("Executing server with command line: " + execLine);
        _solverProcess = Runtime.getRuntime().exec(execLine);

        _solverWatchThread = new Thread(new Runnable() {
            public void run() {
            boolean interrupted;
            do {
                interrupted = false;
                try { _solverProcess.waitFor(); }
                catch (InterruptedException e) { interrupted = true; }
            } while (interrupted);
            }
        });

        _solverWatchThread.setName("BLPSolver internal: solver watch thread");
        _solverWatchThread.start();

        _solverOutputReaderThread = new Thread(new Runnable() {
            public void run() {
            while (_solverIsAlive()) {
                String s = null;
                try  { s = _processOut.readLine(); }
                catch (Exception e) {
                }
            }
            }
        });
        _solverOutputReaderThread.setName ("BLPSolver internal: solver output reader thread");
        _solverOutputReaderThread.start();

      } catch (IOException e) { Dbg.fatal("Could not start solver: ", e); }
    }

    int portnum = PORTNUM;
    try {
        if (_portFile != null) {
        // read port to run on from given file
        try {
            BufferedReader pfile = new BufferedReader (new FileReader (_portFile));
            String portnumline = pfile.readLine ();
            portnum = Integer.parseInt (portnumline);
        }
        catch (FileNotFoundException e) {
            Dbg.fatal ("Could not read port number from file " + _portFile, e);
        }
        }
        _solverSocket = new Socket ("localhost", portnum);
    }
    catch (UnknownHostException e) {
        Dbg.fatal ("Could not connect to solver on port " + portnum + ": ",  e);
    }
    catch (IOException ee) {
        Dbg.fatal ("Could not create socket to connect to solver on port" + portnum + ": ",  ee);
    }
    catch (SecurityException eee) {
        Dbg.fatal ("Could not connect to solver (security): ",  eee);
    }


    try {
        _solverStdIn =
        new PrintWriter(new OutputStreamWriter(_solverSocket.getOutputStream()));
        _solverStdOut =
        new LineNumberReader(new InputStreamReader(_solverSocket.getInputStream()));
        if (RUN_SATSERVER)
        _processOut = new LineNumberReader(new InputStreamReader(_solverProcess.getInputStream ()));

    } catch (IOException e) { Dbg.fatal("Could not create streams for communicating with sovler: ", e); }
    }


    /** Tests whether the solver process is still running. */
    private boolean _solverIsAlive() {
    if (RUN_SATSERVER) {
        return
        _solverProcess!=null &&
        _solverWatchThread != null &&
        _solverWatchThread.isAlive();
    }
    else return true;
    }

    /** If the solver process is running, kill it by sending it an "exit" command. */
    protected void _killProcess() {
    Dbg.info ("Killing solver");
    if (_solverIsAlive()) {
        _sendSolverCmd(BLPSolverCommands.quit ());
        // System.out.println("Waiting for solver process to finish...");
        long curTime = System.currentTimeMillis();
        while (_solverIsAlive() && System.currentTimeMillis() < curTime+600)
        ;
        try {
        _solverSocket.close ();
        } catch (IOException e) {
        Dbg.warn ("got IOException while trying to close socket in killing PSolver", e);
        }
    }
    if (RUN_SATSERVER) {
        if (_solverIsAlive())
        _solverProcess.destroy();  // may not work on Windows
    }
    _solverProcess = null;
    _solverWatchThread = null;
    _solverSocket = null;
    _solverStdIn = null;
    _solverStdOut = null;
    } // _killProcess()

    /**
     * Solve a .sat instance.
     *
     * @return {@link #BL_UNSAT}, {@link #BL_SAT}, {@link #BL_CANCELLED}, or {@link #BL_ERR}.
     *         If {@link #BL_SAT} is returned, {@link #getLastSolution} may be called to
     *         retrieve the satisfying assignment, and {@link #next} may be called to
     *         enumerate subsequent satisfying assignment. */
    protected int _solve(BooleanFormula formula_,
             int nvars_, boolean[] dependentVars_,
             String solverName_,
             boolean enum_,
             long randSeed_ /* ignored for now */,
             int runType_  /* ignored for now */,
             File primVarFileHandle_ /* ignored for now */)
             throws EnvFailureException
    {
    if (true) throw new Error("this code is broken and needs to be reviewed");
    if (RUN_SATSERVER && _solverIsAlive()) _killProcess();
    //_startSolver(configFileName_, solverName_);
    _checkSolver();

    synchronized(this) {
        if (_solveInProgress || _cancelInProgress)
        return BL_CANCELLED;
        _solveInProgress = true;
        _cancelInProgress = false;
    }


    final File problemFileHandle = TmpFiles.createHandleToATempFile("clauses.sat");
    final File solutionFileHandle = TmpFiles.createHandleToATempFile("solution.slv");
    formula_.writeSatFile(problemFileHandle, nvars_, dependentVars_);
    //System.exit(0);
    _sendSolverCmd(BLPSolverCommands.solve (problemFileHandle, solutionFileHandle, TIMEOUT_INTERVAL, PROGRESS_INTERVAL, false));
    _lastNumVars = nvars_;
    return _talkToRunningSolver(nvars_, solutionFileHandle);
    }

    private int _talkToRunningSolver(int nvars_, File solutionFileHandle_) {
        int resultVal = BL_ERR;

        while (resultVal == BL_ERR) {
            // System.out.println ("new loop: " + resultVal);
            BLPSolverMessage result = _getSolverResult();
            if (result.isBlank ()) { // no new message
              //Dbg.info ("No message\n");
                continue;
            }

            //if (result.isStatus ())
            //System.out.println (result.getStatusMessage ());
            if (result.isProgress ()) {
                int progressVal = result.getProgressValue ();
                //System.out.println("Progress report: " + progressVal);
                Thread.yield();
                // if (progressVal == 100) System.out.println();
            }

            Thread.yield();  // give GUI time to update

            if (result.isSolution ()) {
                if (result.getSolutionType () == BLPSolverMessage.SAT) {
                    resultVal = BL_SAT;
                    Dbg.info("GOT RESULT: SAT");
                }
                else {
                    resultVal = BL_UNSAT;
                    Dbg.info("GOT RESULT: UNSAT");
                }
            }
            else if (result.isCancelled () || result.isTimeout ())
                resultVal = BL_CANCELLED;
            else if (result.isAcknowledged ()) {
                _clientId = result.getClientId ();
                Dbg.info ("Got ack, id: " + _clientId);
            }
        }

        _lastResult = resultVal;
        try {
            LineNumberReader solReader = new LineNumberReader(new FileReader(solutionFileHandle_));
            _lastSolution = (resultVal == BL_SAT) ?
                _readAssignmentFrom(solReader, nvars_) : null;
        } catch (IOException ioe_) {
            Dbg.fatal("Error reading solution:", ioe_);
        }
        // System.out.println("lastSolution ok");

        synchronized(this) {
            _solveInProgress = false;
            _cancelInProgress = false;
            if (RUN_SATSERVER) _killProcess();
            return resultVal;
        }
    }  // public void solve()


    /** Get next solution, if last solve() returned BL_SAT */
    protected int _next() {
        File solutionFileHandle = TmpFiles.createHandleToATempFile("solution.slv");
        _sendSolverCmd(BLPSolverCommands.next (_clientId));
        return _talkToRunningSolver(_lastNumVars, solutionFileHandle);
    }

    /** Cause a currently running {@link #solve} or {@link #next} to quit immediately,
    returning {@link #BL_CANCELLED}. */
    protected void _interruptSolver() {
        if (_solveInProgress && !_cancelInProgress) {
            _cancelInProgress = true;
            _sendSolverCmd(BLPSolverCommands.cancel (_clientId));
        }
    }

    /** check that the solver is alive, cause assertion failure if not */
    private void _checkSolver() {
        Dbg.chk(_solverIsAlive(), "PSolver process crashed");
    }

}  // class BLSATLab
